perm filename REDUCT[E82,JMC] blob sn#677231 filedate 1982-09-11 generic text, type C, neo UTF8
COMMENT āŠ—   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	reduct[e82,jmc]		reduction to satisfiability and satisfiability machine
C00003 ENDMK
CāŠ—;
reduct[e82,jmc]		reduction to satisfiability and satisfiability machine

1. One kind of length of proof is the number of steps to reduce the
problem to proving the non-satisfiability of a propositional
formula.  This comes from considering the form of lemmas that
might be proved in showing that  8 queens has just the known
solutions.  The simpler lemmas exclude squares, but the more
complex yield disjunctions.

2. This being true, perhaps the key hardware problem is to design
a parallel satisfiability machine.